minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
↳ QTRS
↳ DependencyPairsProof
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
QUOT2(s1(x), s1(y)) -> QUOT2(minus2(x, y), s1(y))
PLUS2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> PLUS2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
PLUS2(s1(x), y) -> PLUS2(x, y)
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
QUOT2(s1(x), s1(y)) -> MINUS2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
QUOT2(s1(x), s1(y)) -> QUOT2(minus2(x, y), s1(y))
PLUS2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> PLUS2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
PLUS2(s1(x), y) -> PLUS2(x, y)
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
QUOT2(s1(x), s1(y)) -> MINUS2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
PLUS2(s1(x), y) -> PLUS2(x, y)
PLUS2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> PLUS2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS2(s1(x), y) -> PLUS2(x, y)
Used ordering: Polynomial interpretation [21]:
PLUS2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> PLUS2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
POL(0) = 0
POL(PLUS2(x1, x2)) = 2·x1 + 2·x2
POL(minus2(x1, x2)) = x1
POL(s1(x1)) = 1 + 2·x1
minus2(s1(x), s1(y)) -> minus2(x, y)
minus2(x, 0) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
PLUS2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> PLUS2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS2(s1(x), s1(y)) -> MINUS2(x, y)
POL(MINUS2(x1, x2)) = 2·x2
POL(s1(x1)) = 2 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
QUOT2(s1(x), s1(y)) -> QUOT2(minus2(x, y), s1(y))
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT2(s1(x), s1(y)) -> QUOT2(minus2(x, y), s1(y))
POL(0) = 0
POL(QUOT2(x1, x2)) = 2·x1
POL(minus2(x1, x2)) = 2·x1
POL(s1(x1)) = 2 + 2·x1
minus2(s1(x), s1(y)) -> minus2(x, y)
minus2(x, 0) -> x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
minus2(x, 0) -> x
minus2(s1(x), s1(y)) -> minus2(x, y)
quot2(0, s1(y)) -> 0
quot2(s1(x), s1(y)) -> s1(quot2(minus2(x, y), s1(y)))
plus2(0, y) -> y
plus2(s1(x), y) -> s1(plus2(x, y))
plus2(minus2(x, s1(0)), minus2(y, s1(s1(z)))) -> plus2(minus2(y, s1(s1(z))), minus2(x, s1(0)))